Nuprl Lemma : Rall-has-loc
11,40
postcript
pdf
L
:(top List),
R
,
i
:top.
sqequal(R-has-loc(Rall(
L
;
x
.
R
(
x
));
i
); reduce((
x
,
b
. bor(R-has-loc(
R
(
x
);
i
);
b
)); ff;
L
))
latex
Definitions
Y
,
map(
f
;
as
)
,
reduce(
f
;
k
;
as
)
,
t
T
,
Rall(
L
;
x
.
R
(
x
))
,
top
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
,
map
wf
,
Rlist-has-loc
origin
L:(top List), R,i:top.
x,b. bor(R-has-loc(R(x); i); b)); ff; L)) L:(top List), R,i:top.
x,b. bor(R-has-loc(R(x); i); b)); ff; L)) 
Tx:A. B(x)